Reported by [email protected], Jan 10, 2014

The following is suggested for Data.Sign.Properties and
Data.Integer, Data.Integer.Properties.

1. For Data.Sign :

   _s-assoc : Associative _s
   _s-comm : Commutative _s
   *s-invol : (s : Sign) → s *s s ≡ Sign.+

This is for *s = Sign.*.
I use these lemmata, and they are evidently of a general use.

1. For Data.Integer, Data.Integer.Properties :

divMod is desirable for division with remainder, with proofs.

It can be lifted from Nat.DivMod.divMod.
But this lift still needs implementation.

For example, I need

decDivide : (x y : ℤ) → Dec $ RightQuotient intSetoid * x y

-- which also returns proof/disprove for \exist \q -> y * q == y.
It can be either by calling Integer.divMod
or by lifting to ℤ from a similar decDivide-Nat for Nat.
My implementation for this lifting takes about 200 lines
(despite that the subject looks trivial).

I think, Integer.divMod will help in this and in many other cases,
and I suspect that its lifting to ℤ will take not less than 100 lines.

1. The following are useful :

   negneg : (x : ℤ) → - (- x) ≡ + x

   x+◃ : (m : ℕ) → (Sign.+ ◃ m) ≡ + m
   -◃ : (m : ℕ) → (Sign.- ◃ m) ≡ - (+ m)

   +m*+n= : (m n : ℕ) → (+ m) * (+ n) ≡ + (m *n n)

   -*- : (x y : ℤ) → (- x) * (- y) ≡ x * y

   s◃m*s'◃n : (s s' : Sign) → (m n : ℕ) →
   (s ◃ m ) * (s' ◃ n) ≡ (s *s s') ◃ (m *n n)

(for the last one I have a proof of about 30 lines).